g:IMonoid, a, b, c:.
(a  b)
 (b  c)
 (E:({a..c}|g|).
 (*,e) a  j < c. E(j) = ((*,e) a  j < b. E(j) * (*,e) b  j < c. E(j))  |g|) 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	t  T, x:A. B(x), False, A, P & Q, i  j < k, x. t(x), {T}, , x f y, x(s), {i..j}, A  B, P  Q, P  Q, P  Q, True, T, {i...}, IMonoid
Lemmas	imon wf, int upper wf, grp id wf, grp op wf, itop wf, grp car wf, int seg wf, le wf, int le to int upper, int upper ind, mon ident, itop unroll base, mon assoc, itop unroll hi, itop unroll lo, true wf, squash wf